Managing Citizen Profiles in the Domain of e-Government: The cPortfolio Project

The provision of support for holistic operations in the scope of a horizontal digital administration requires the fulfillment of a number of previous steps that guarantee the viability of services in the domain. One of these tasks is the proper management of documents. Documents are a key element of any democratic administration and their digital management is a clear pre-requisite for the arrival of digital government. This article tackles how this service can be provided using the support of semantics as a technological cornerstone. The implementation of such a tool is made through the so-called cPortfolio. This platform is deeply discussed and details about its design and implementation are provided. This system is designed to manage both the personal information from the citizen and the documents they possess. Tests on the prototype showed interesting features regarding the simplicity of use and the interoperability support provided to third party agents.     

面向网格监控的工作流建模研究

网格监控系统种类繁多而且大多具有自身特定的应用领域,有必要对一般性的网格监控模块提供设计参考及相应分析评价方法。文中提出基于活动网络图为网格监控的数据处理流程建立工作流模型并进行语义描述。通过阐释网格监控架构和具有代表性的网格监控系统,总结分析了3种监控过程的一般数据流程,为典型的数据处理流程设计了工作流模型,给出了主要工作流模型的形式化说明。此建模方法有助于网格监控模块的设计,同时为面向网格监控的信息处理过程的分析与评价提供了一种可供参考的形式化语义。     

维吾尔语框架语义知识库的概念设计

该文对维吾尔语的框架语义描述体系及内容进行了初步探讨和尝试,建立了维吾尔语框架语义文档的树型结构。根据维吾尔语框架语义知识库的描述内容及框架语义网络自身的特点,该文在数据库中以维吾尔语框架语义为核心进行信息存储,设计了语义知识库的概念模型。为创建基于认知的维吾尔语框架语义知识库建设探索了一条可行的技术路线、方法和思路。     

对一种身份认证协议的改进及其形式化分析①

基于口令的远程身份认证协议是目前认证协议研究的热点。2005年,Sung-Woon Lee等人提出了一个低开销的基于随机数的远程身份认证协议即Lee-Kim-Yoo协议,首先分析了此协议中所存在的安全性缺陷,随后构造了一个基于随机数和Hash函数,并使用智能卡的远程身份认证协议,最后用BAN逻辑对修改后的协议进行了形式化的分析,结果表明修改后的协议能够达到协议的安全目标。     

可信计算语义证明模型的研究

针对现有的可信计算平台体系认证技术是静态的、一次性的,并不基于语义等问题,提出了语义远程认证抽象模型,该模型由代码特征化部件、安全监测部件、安全控制部件、应用接口部件、知识库组成。其中关键问题知识库采用离线创建规则的学习模式,供在线检测。     

利用SMT约束分解方法求解RTL可满足性问题

随着集成电路技术与工艺的不断发展,目前工业界所采用的形式验证工具已很难适应集成电路规模的飞速增长.为了对RTL电路的可满足性问题进行形式验证,提出基于超图划分的约束分解实现可满足性模理论(SMT)求解的分级验证方法.通过分析RTL电路的结构约束,对约束集合中的元素和相关变量进行约束建模,并构建带有合适权重的超图模型;利用超图划分的机制寻找带有最小割集的等量划分,实现约束分解,完成RTL电路的定界模型检验.实验结果表明,该方法能够减小处理问题的规模和求解过程中的搜索空间,提高验证效率.     

Ready to preorder: The case of weak process semantics

Recently, Aceto, Fokkink and Ingólfsdóttir proposed an algorithm to turn any sound and ground-complete axiomatisation of any preorder listed in the linear time-branching time spectrum at least as coarse as the ready simulation preorder, into a sound and ground-complete axiomatisation of the corresponding equivalence—its kernel. Moreover, if the former axiomatisation is ω-complete, so is the latter. Subsequently, de Frutos Escrig, Gregorio Rodríguez and Palomino generalised this result, so that the algorithm is applicable to any preorder at least as coarse as the ready simulation preorder, provided it is initials preserving. The current paper shows that the same algorithm applies equally well to weak semantics: the proviso of initials preserving can be replaced by other conditions, such as weak initials preserving and satisfying the second τ-law. This makes it applicable to all 87 preorders surveyed in “the linear time-branching time spectrum II” that are at least as coarse as the ready simulation preorder. We also extend the scope of the algorithm to infinite processes, by adding recursion constants. As an application of both extensions, we provide a ground-complete axiomatisation of the CSP failures equivalence for BCCS processes with divergence.     

Evaluation of Localized Semantics: Data, Methodology, and Experiments

We present a new data set of 1014 images with manual segmentations and semantic labels for each segment, together with a methodology for using this kind of data for recognition evaluation. The images and segmentations are from the UCB segmentation benchmark database (Martin et al., in International conference on computer vision, vol. II, pp. 416–421, 2001). The database is extended by manually labeling each segment with its most specific semantic concept in WordNet (Miller et al., in Int. J. Lexicogr. 3(4):235–244, 1990). The evaluation methodology establishes protocols for mapping algorithm specific localization (e.g., segmentations) to our data, handling synonyms, scoring matches at different levels of specificity, dealing with vocabularies with sense ambiguity (the usual case), and handling ground truth regions with multiple labels. Given these protocols, we develop two evaluation approaches. The first measures the range of semantics that an algorithm can recognize, and the second measures the frequency that an algorithm recognizes semantics correctly. The data, the image labeling tool, and programs implementing our evaluation strategy are all available on-line (kobus.ca//research/data/IJCV_2007). We apply this infrastructure to evaluate four algorithms which learn to label image regions from weakly labeled data. The algorithms tested include two variants of multiple instance learning (MIL), and two generative multi-modal mixture models. These experiments are on a significantly larger scale than previously reported, especially in the case of MIL methods. More specifically, we used training data sets up to 37,000 images and training vocabularies of up to 650 words. We found that one of the mixture models performed best on image annotation and the frequency correct measure, and that variants of MIL gave the best semantic range performance. We were able to substantively improve the performance of MIL methods on the other tasks (image annotation and frequency correct region labeling) by providing an appropriate prior.     

The Basic Constructive Logic for Negation-Consistency

In this paper, consistency is understood in the standard way, i.e. as the absence of a contradiction. The basic constructive logic B_Kc4, which is adequate to this sense of consistency in the ternary relational semantics without a set of designated points, is defined. Then, it is shown how to define a series of logics by extending B_Kc4 up to minimal intuitionistic logic. All logics defined in this paper are paraconsistent logics.     

Test frame updating in CPM testing of Prolog programs

Category Partition Method (CPM) is a general approach to specification-based program testing, where test frame reduction and refinement are two important issues. Test frame reduction is necessary since too many test frames may be produced, and test frame refinement is important since during CPM testing new information about test frame generation may be achieved and considered incrementally. Besides the information provided by testers or users, implementation related knowledge offers alternative information for reducing and refining CPM test frames. This paper explores the idea by proposing a call patterns semantics based test frame updating method for Prolog programs, in which a call patterns analysis is used to collect information about the way in which procedures are used in a program. The updated test frames will be represented as constraints. The effect of our test frame updating is two-fold. On one hand, it removes “uncared” data from the original set of test frames; on the other hand, it refines the test frames to which we should pay more attention. The first effect makes the input domain on which a procedure must be tested a subset of the procedure’s input domain, and the latter makes testers stand more chance to find out the faults that are more likely to show their presence in the use of the program under consideration. Our test frame updating method preserves the effectiveness of CPM testing with respect to the detection of faults we care. The test case generation from the updated set of test frames is also discussed. In order to show the applicability of our method an approximation call patterns semantics is proposed, and the test frame updating on the semantics is illustrated by an example.